\section{Evolving Systems}
\label{sec:Evolving}

The File System of \Fig \ref{fig:naivefs} was not ensuring any property we were interested in. This Section presents two interesting iterations: the first step leads to a \emph{simple File System} $\FSS$ that matches Requirement \textbf{\texttt{R1}}, \ie files can be opened only by users with sufficient access rights; the second iteration leads to a \emph{Confined File System} $\FSC$ that matches Requirement \textbf{\texttt{R2}}, \ie it further ensures the confinement property on file opening. 

%The additional abstract data types for each version of the \textsc{Fs} as well as the precise definition of the required morphisms to ensure a correct iteration can be found in \cite{lucio:10}.

\subsection{Simple File System \emph{$\FSS$}}
\label{sec:Evolving-Simple}

\begin{figure}[t]
	\centering
  \epsfig{file=images/simple_security_fs, width=\linewidth}
	\caption{Simple security filesystem. Same initial marking as \Fig\ref{fig:naivefs}.}
	\label{fig:simplesec}

	\vspace{-0.4cm}
\end{figure}

The \textsc{Fs} of \Fig \ref{fig:MLS-M} was naive in the sense that it simply implements the basic mechanisms for opening / reading and closing files, without access control. We make $\FS$ evolve into $\FSS$ to meet Requirement \textbf{\texttt{R1}} by guarding each file use (either reading or writing) by a condition that checks the access rights: in \Fig \ref{fig:simplesec}, each transition ($\mathtt{openR}$, $\mathtt{openW}$, $\mathtt{closeR}$ or $\mathtt{closeW}$) is now guarded to prevent the firing if the $\mathtt{\$u}$'s access class does not dominate $\mathtt{\$f}$'s access class. 

From a specification point of view, the corresponding \textsc{Apn} $\FSS\in\mathcal{N}$ is componentwise identical to $\FS\in\mathcal{N}$, except for the guards. More formally, we have:

\begin{scriptsize}
\begin{displaymath}
%\hspace{-0.4cm} 
	cond_{\mathsf{FSS}} = \left\{\begin{array}{r@{\;\mapsto\;}l}
		\mathsf{reading}, \mathsf{writing} & \{\mathsf{dominates(class(\$u), class(\$f)) = true}\}\\
		\mathsf{closeR}, \mathsf{closeW} & \{\mathsf{name(\$u) = name(second(\$f))}\}	\end{array}\right\}\end{displaymath}\end{scriptsize}

In this iteration, the \textsc{Pn}'s structure does not change: no places are added or removed; therefore the morphism is simply the identity: $f_{\mathsf{PP}} = id$. Nevetheless, the transitions are strengthened by new guards that straightforwardly imply the previous empty guards ($cond_{\mathsf{FSS}} \Longrightarrow cond_{\mathsf{FS}}$). Table \ref{tab:satisfaction} (Row 2) summarises the iteration when model-checking all properties on $\FSS$: $\mathtt{P1}$ and $\mathtt{P2}$ now hold.


\subsection{Confined File System \emph{$\FSC$}}
\label{sec:Evolving-Confined}

We now make $\FSS$ evolve into $\FSC$ to prevent Trojan horses attacks happening, thus meeting Requirement \textbf{\texttt{R2}}. Two new places $\mathtt{logRead}$ and $\mathtt{logWrite}$ are added: they log a list of pairs $(\mathtt{\$f}, \mathtt{\$u})$, adding an element each time $\mathtt{\$u}$ opens $\mathtt{\$f}$ and deleting it when closed, for each opening mode. Every time a \emph{new} file is opened in read mode, $\mathtt{openRead}$ checks from $\mathtt{logWrite}$ if no file with smaller access rights is open by the same user in write mode. We introduce a new function $\mathtt{min(\$lfu)}$ that computes the minimum access class (for the domination) in the list $\mathtt{\$lfu}$ of pairs $(\mathtt{\$f}, \mathtt{\$u})$. The new guard for the $\mathtt{openRead}$ transition is now a conjunction of the previous guard with a new condition stating that the minimal access class in $\mathtt{logWrite}$ dominates the newly opened file. The reverse principle is applied for $\mathtt{openWrite}$ with a function $\mathtt{max}$ retrieving the maximal access class logged in $\mathtt{logRead}$. The corresponding \textsc{Adt} is defined as follows:

\noindent
\begin{center}
	\begin{minipage}[b]{0.9\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
import "file.adt"
import "user.adt"
import "accessClass.adt"
import "pair.gadt"
import "list.gadt"
import "fileUserPair"
Adt listOfFiles is list[FileUserPair]
	Operations
		maxAccess : list[FileUserPair] -> accessClass;
		calcMaxAccess : accessClass, list[FileUserPair] -> accessClass;

		minAccess : list[FileUserPair] -> accessClass;
		calcMinAccess : accessClass, list[FileUserPair] -> accessClass;
	Axioms
		maxAccess($l) = calcMaxAccess(first($l),$l);		

		calcMaxAccess($acl,empty) = $acl;
		if (class(first($p)) dominates $acl) = true then
				calcMaxAccess($acl,list($p,$l))=calcMaxAccess(class(first($p)),$l);
		if ($acl dominates getAccessClass(first($p))) = true then
			calcMaxAccess($acl,list($p,$l)) = calcMaxAccess($acl,$l);
		
		minAccess($l) = calcMinAccess(first($l),$l);	
					
		calcMinAccess($acl,empty) = $acl;
		if (class(first($p)) dominates $acl) = true then
			calcMinAccess($acl,list($p,$l)) = calcMinAccess($acl,$l);
		if ($acl dominates class(first($p))) = true then
			calcMinAccess($acl,list($p,$l)) = calcMinAccess(class(first($p)),$l);
	Variables
		l   : list[FileUserPair];
		p   : FileUserPair;
		acl : accessClass;
		\end{lstlisting}
	\end{minipage}
\end{center}


The \textsc{Apn} $\FSC\in\mathcal{N}$ is defined as follows:
\begin{itemize}
	\item $\Sigma_{\mathsf{FSC}}$ is the same as $\Sigma_{\mathsf{FS}}$ with the additional \textsc{Adt} \textsf{listOfFiles}, and $A_{\mathsf{FSC}}$ the corresponding initial algebra;
	
	\item From \Fig \ref{fig:confinedfs}, we have 
\begin{displaymath}
\begin{array}{r@{\;=\;}l}
P_{\mathsf{FSC}} & P_{\mathsf{FS}} \cup \{\mathtt{logRead}, \mathtt{logWrite}\}\\
T_{\mathsf{FSC}} & T_{\mathsf{FS}}	
	\end{array}\end{displaymath}
	
	\item the input/output arcs for each transition are those previously defined for $\FS$, plus those coming from respectively $\mathsf{logWrite}$ and $\mathsf{logRead}$:

	\begin{scriptsize}
\begin{displaymath}
\hspace{-0.8cm} 
\begin{array}{rcl}
	pre_{\mathsf{FSC}} &\!\!\!\!=\!\!\!\!& \left\{\begin{array}{r@{\;\mapsto\;}l}
		\mathsf{openR} & pre_{\mathsf{FS}}(\mathsf{openR}) \oplus [(\mathsf{\$lpw}, \mathsf{logWrite})];\\
		\mathsf{openW} & pre_{\mathsf{FS}}(\mathsf{openW}) \oplus [(\mathsf{\$lpw}, \mathsf{logRead})];\\
		\mathsf{closeR} & pre_{\mathsf{FS}}(\mathsf{closeR}) \oplus [(\mathsf{\$lpr}, \mathsf{logRead})];\\
		\mathsf{closeW} & pre_{\mathsf{FS}}(\mathsf{closeW}) \oplus [(\mathsf{\$lpr}, \mathsf{logWrite})];
		\end{array}\right\}\\
\\
	post_{\mathsf{FSC}} &\!\!\!\!=\!\!\!\!& \left\{\begin{array}{r@{\;\mapsto\;}l}
		\mathsf{openR} & post_{\mathsf{FS}}(\mathsf{openR}) \oplus [(\mathsf{list(pair(\$f,\$u), \$lpr)}, \mathsf{logRead})];\\
		\mathsf{openW} & post_{\mathsf{FS}}(\mathsf{openW}) \oplus [(\mathsf{list(pair(\$f,\$u), \$lpw)}, \mathsf{logWrite})];\\
		\mathsf{closeR} & post_{\mathsf{FS}}(\mathsf{closeR}) \oplus [(\mathsf{delete(\$p, \$lpr)}, \mathsf{logRead})]\\
		\mathsf{closeW} & post_{\mathsf{FS}}(\mathsf{closeW}) \oplus [(\mathsf{delete(\$p, \$lpr)}, \mathsf{logWrite})]%
\end{array}\right\}
\end{array}\end{displaymath}\end{scriptsize}

	\item The guards for transitions $\mathsf{closeR}$ and $\mathsf{closeW}$ are the same as previously; those for the added transitions $\mathsf{logRead}$ and $\mathsf{logWrite}$ are empty; and the guards for $\mathsf{openR}$ and $\mathsf{openR}$ are enforced accordingly:
	
	\begin{scriptsize}
\begin{displaymath}
\hspace{-0.8cm} 
		cond_{\mathsf{FSC}} = \left\{\begin{array}{r@{\;\mapsto\;}l}
		\mathsf{logRead}  & \emptyset\\
		\mathsf{logWrite} & \emptyset\\
		\mathsf{openR} & \left\{\begin{array}{l}
			\mathsf{dominates(class(\$u), class(\$f)) = true} \;\;\mathsf{\&} \\
			\mathsf{dominates(minAccess(\$lpw), class(\$f)) = true} 
		\end{array}\right\}\\
		\mathsf{openW} & \left\{\begin{array}{l}
			\mathsf{dominates(class(\$u), class(\$f)) = true} \;\;\mathsf{\&} \\
			\mathsf{dominates(class(\$f), maxAccess(\$lpr)) = true} 
		\end{array}\right\}\\
		\mathsf{closeR} & cond_{\mathsf{FS}}(\mathsf{closeR})\\								\mathsf{closeW} & cond_{\mathsf{FS}}(\mathsf{closeW})	\end{array}\right\}\end{displaymath}\end{scriptsize}	
\end{itemize}

We now define the morphism $f\in\mathcal{M}(\FSS, \FSC)$ for this iteration. Since $\FSC$ had been defined by extending $\FSS$, the morphism only consists of mapping the previous structure into the extended ones:
\begin{itemize}
	\item $f_\Sigma$ maps sorts, operations and equations to the syntactically corresponding ones: sort $\mathsf{fileName}$ in $\FSS$ is mapped to sort $\mathsf{fileName}$ in $\FSC$ and so one, and the same for operations and equations; 
	\item $f_A$ naturally maps terms syntactically;
	\item $f_P$ and $f_T$ map places and transitions using name correspondance: place $\mathsf{files}$ in $\FSS$ is mapped to place $\mathsf{files}$ in $\FSC$, and so on.
\end{itemize}
We still have to check that conditions from Def. \ref{def:PP-GS} hold for $f$. We briefly comment on each of these conditions:
\begin{itemize}
	\item w.r.t. the note following Def. \ref{def:PP-GS}, firing conditions are preserved due to the guard strengthening;
	\item comparing \Fig \ref{fig:simplesec} and \Fig \ref{fig:confinedfs} and their formal specifications, no new arcs are added to the places already present in $\FSS$;
	\item Obviously from their definition, $f_T$, $f_P$ and $f_\Sigma$ are injections and $f_\Sigma$ is persistent since $\Sigma_{\mathsf{FSS}} \subseteq \Sigma_{\mathsf{FSC}}$;
	\item $\FSC$ is an embedding of $FSC$ according to the definition of $\FSC$ by extension of $\FSS$ for $pre$ and $post$;
	\item $A_{\mathsf{FSC}}$ is a correct extension of $A_{\mathsf{FSS}}$ with no renaming.
\end{itemize}
These constitute a safe iteration from $\FSS$ to $\FSC$ because the corresponding morphisms match the conditions of \Sect \ref{sec:Preservation}. Table \ref{tab:satisfaction} (Row 3) summarises the model-checking of all properties on $\FSC$: $\mathtt{P1}$ and $\mathtt{P2}$ still hold; $\mathtt{P3}$ is now satisfied.


\begin{figure}[t]
	\centering
  \epsfig{file=images/confined_fs, width=\linewidth}
	\caption{Confined filesystem. Same initial marking as \Fig\ref{fig:naivefs}.}
	\label{fig:confinedfs}

\vspace{-0.4cm}
\end{figure}
